#include"cnf.h"
#include"dpll.h"
#include"common.h"
#include"dpll_pthread.h"
#include"solver.h"
#include<stdio.h>
#include "dimac_parser.h"
//#include "dpll_openmp.h"
#include "cdcl.h"

#ifdef MPI_CDCL
#include<mpi.h>
solver dpll_solver = {
    .SATISFIABLE = &mpi_cdcl_satisfiable,
    .get_cnf = NULL,
};
#endif
#ifdef BASIC_CDCL
solver dpll_solver = {
    .SATISFIABLE = &cdcl_satisfiable,
    .get_cnf = NULL,
};
#endif
#ifdef USE_OMP
solver dpll_solver = {
    .SATISFIABLE = &dpll_satisfiable_omp,
    .get_cnf = NULL,
};
#endif
#ifdef USE_PTHREAD
solver dpll_solver = {
    .SATISFIABLE = &dpll_satisfiable_pth,
    .get_cnf = NULL,
};
#endif
#ifdef BASIC
solver dpll_solver = {
    .SATISFIABLE = &dpll_satisfiable,
    .get_cnf = NULL,
};
#endif
int CERR_LEVEL = 0;
cnf cnf_1;
//timer tm;
long long threshold = 0;
#define LINUX
//#define WINDOWS
//#define huawei
const char* filenames[] = {
#ifdef huawei
    "/home/s1811349/simd_hm/data/uf75-01.cnf",
    "/home/s1811349/simd_hm/data/uf75-02.cnf",
    "/home/s1811349/simd_hm/data/uf75-03.cnf",
    "/home/s1811349/simd_hm/data/uf75-04.cnf",
    "/home/s1811349/simd_hm/data/uf75-05.cnf",
#endif
#ifdef LINUX
    "/media/dongjialin/disk1/Parallel/hm/hm2/self_testcases/test2.cnf",
    "/media/dongjialin/disk1/Parallel/hm/hm2/self_testcases/test1.cnf",
    "/media/dongjialin/disk1/Parallel/hm/hm2/uf20-91/uf20-01.cnf",
    "/media/dongjialin/disk1/Parallel/hm/hm2/uf20-91/uf20-02.cnf",
    "/media/dongjialin/disk1/Parallel/hm/hm2/uf20-91/uf20-03.cnf",
    "/media/dongjialin/disk1/Parallel/hm/hm2/uf50-218/uf50-01.cnf",
    "/media/dongjialin/disk1/Parallel/hm/hm2/uf50-218/uf50-0942.cnf",
    "/media/dongjialin/disk1/Parallel/hm/hm2/UUF75.325.100/uuf75-01.cnf",
    "/media/dongjialin/disk1/Parallel/hm/hm2/UUF75.325.100/uuf75-02.cnf",
    "/media/dongjialin/disk1/Parallel/hm/hm2/UUF100.430.1000/uuf100-01.cnf",
    "/media/dongjialin/disk1/Parallel/hm/hm2/uf100-430/uf100-01.cnf",
    "/media/dongjialin/disk1/Parallel/hm/hm2/uf100-430/uf100-02.cnf",
    "/media/dongjialin/disk1/Parallel/hm/hm2/uf75-325/uf75-05.cnf",
#endif
#ifdef WINDOWS
    "E:\\Parallel\\hm\\hm2\\UUF75.325.100\\uuf75-08.cnf",
    "E:\\Parallel\\hm\\hm2\\UUF100.430.1000\\uuf100-013.cnf",
#endif
};
char* filename;
dimac_parser* parser;
int main(int argc, char *argv[]){
    //choose file
    //tm.totime = 0;
#ifndef MPI_CDCL
    filename = filenames[12];
    printf("file:%s\n", filename);
    parser = parser_init(filename);
    init_ori_cnf(&cnf_1);
    parse(parser, &cnf_1);
    print_cnf(&cnf_1);
    // for(int i = 0; i < cnf_1.nclause; i++){
    //     printf("@@@ %d\n", cnf_1.clause_start[i]);
    // }
    //timer_start(&tm);
    if(dpll_solver.SATISFIABLE(&cnf_1)){
        printf("found a solution\n");
    }
    else{
        printf("didn't found any solution\n");
    }
    //timer_stop_n_accum(&tm);
    //printf("%s use time %lld us\n", filename, tm.tottime);
    printf("threshold %lld\n", threshold);
#endif 
#ifdef MPI_CDCL
    MPI_Init(&argc, &argv);
    int rank;
    _bool sat;
    MPI_Comm_rank(MPI_COMM_WORLD, &rank); 
    init_mpi_datatype();
    filename = filenames[10];
    printf("file:%s\n", filename);
    parser = parser_init(filename);
    init_ori_cnf(&cnf_1);
    parse(parser, &cnf_1);
    assert(rank < 32);
    if (rank == 0){
        print_cnf(&cnf_1);    
        sat = mpi_cdcl_satisfiable(&cnf_1, rank);
    }
    else{
        assert(rank < 32);
        mpi_cdcl_satisfiable(&cnf_1, rank);
    }

    MPI_Finalize();
#endif
   
   // system("pause");
}